Nuprl Definition : combine-ecl-tuples2 11,40

combine-ecl-tuples2(A; B; f; g)
== spreadn(A;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(B;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(Tb,ksb,ib,gb,hb,ab,eb.<:Ta  (:Tb  (?))
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, append(ksa; ksb)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, <ia, ib, inr  >
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let sa = if deq-member(Kind-deq; k'; ksa)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let then ga(k',s,v,x.1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let else x.1
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let fi  in
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet sb = if deq-member(Kind-deq; k'; ksb)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet then gb(k',s,v,(x.2).1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet else (x.2).1
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet fi  in
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet f<sa
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , sb
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info(ea;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info(eb;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info((m.ha(m,sa));
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info((m.hb(m,sb));
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info((x.2.2))>
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,x. f((x.2.2),m.ha(m,x.1),m.hb(m,(x.2).1),n)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. g
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. (ha(0,x.1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,hb(0,(x.2).1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,reduce((m,b. bor((ha(m,x.1)); b)); ff; ea)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,reduce((m,b. bor((hb(m,(x.2).1)); b));
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,reduce(ff;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,reduce(eb)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,if deq-member(Kind-deq; k'; ksa)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,then aa(n,k',s,v,x.1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,else ff
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,fi 
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,if deq-member(Kind-deq; k'; ksb)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,then ab(n,k',s,v,(x.2).1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,else ff
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,fi )
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, merge(ea; eb)>)) 
latex



clarification:

combine-ecl-tuples2(A; B; f; g)
== spreadn(A;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(B;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(Tb,ksb,ib,gb,hb,ab,eb.<:Ta  (:Tb  ( + Unit))
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, append(ksa; ksb)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, <ia, ib, inr  >
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let sa = if deq-member(Kind-deq; k'; ksa)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let then ga(k',s,v,x.1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let else x.1
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let fi  in
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet sb = if deq-member(Kind-deq; k'; ksb)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet then gb(k',s,v,(x.2).1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet else (x.2).1
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet fi  in
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet f<sa
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , sb
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info(ea;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info(eb;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info((m.ha(m,sa));
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info((m.hb(m,sb));
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info((x.2.2))>
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,x. f((x.2.2),m.ha(m,x.1),m.hb(m,(x.2).1),n)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. g
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. (ha(0,x.1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,hb(0,(x.2).1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,reduce((m,b. bor((ha(m,x.1)); b)); ff; ea)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,reduce((m,b. bor((hb(m,(x.2).1)); b));
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,reduce(ff;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,reduce(eb)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,if deq-member(Kind-deq; k'; ksa)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,then aa(n,k',s,v,x.1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,else ff
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,fi 
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,if deq-member(Kind-deq; k'; ksb)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,then ab(n,k',s,v,(x.2).1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,else ff
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,fi )
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, merge(ea; eb)>)) 
latex


Definitionscombine-ecl-tuples2(A; B; f; g), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), , Unit, append(as; bs), , let x = a in b(x), combine-halt-info(ea; eb; f; g; x), reduce(f; k; as), bor(p; q), if b then t else f fi , deq-member(eq; x; L), Kind-deq, t.1, t.2, ff, merge(as; bs)
FDL editor aliasescombine-ecl-tuples2

origin